Nuprl Definition : ma-rframe 0,22

M.rframe(k reads x)
== L != 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))))(x deq-member(KindDeq;k;L
latex



clarification:

M.rframe(k reads x)
== fpf-val(IdDeq;
== fpf-val(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))));
== fpf-val(x;
== fpf-val(x,L.deq-member(KindDeq;k;L)) 
latex


Definitionsz != f(x P(a;z), IdDeq, 1of(t), 2of(t), b, deq-member(eq;x;L), KindDeq
FDL editor aliasesma-rframe

origin